1. Field of the Invention
This invention relates to computer aided design (CAD). In particular, the invention relates to hardware functional verification.
2. Description of Related Art
As technology in computer aided design becomes mature, design verification has become more and more important to ensure design correctness of circuits. In formal design verification, checking logic functionality is a major step.
Approaches to logic checking include functional methods based on Boolean representations, such as Binary Decisions Diagrams (BDDs), and structural methods. Using a symbolic representation of Boolean functions, a generalized form of a problem can be expressed. Solving the generalized form leads to solutions of many specific problem instances. For example, the BDDs provide an efficient method to represent Boolean functions. BDDs are a canonical form, i.e., every Boolean function is represented by only one BDD. In certain approaches, logic checking with BDDs can be reduced to comparing two BDDs, a simple check for equality.
However, traditional approaches using Boolean expressions suffer a major drawback in that the design complexity (in terms of number of hardware elements) can lead to an exponential growth in the size of the BDDs. In traditional symbolic simulation approaches, distinct Boolean variables are applied at each circuit input. The circuit is then simulated until the symbolic output expressions are produced. These expressions are then restricted according to the input constraint(s) expressed by some Boolean predicate. For example, the results of symbolically simulating a floating-point adder with arbitrary inputs could be restricted by the desired constraints on the input nodes (e.g., to prevent illegal inputs, output overflow, or denormalization). As the circuit complexity grows, as is often the case with current designs, traditional approaches become impractical. The design complexity requires that the circuit be simultaneously simulated for all possible inputs with fully calculated outputs.
Jain and Gopalakrishnan (in xe2x80x9cEfficient symbolic simulation-based verification using the parametric form of Boolean expressionxe2x80x9d, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 13, No. 8, August 1994, pp. 1005-1015) discusses the use of symbolic simulation and the parametric form. However, their technique does not work for an arbitrary predicate and does not apply parameterization in performing input space decomposition. Their technique applies only to designs that can be described recursively, and requires that the predicate be transformed to disjunctive normal form, which is impractical or impossible for the complex predicates encountered in industrial circuits.
Therefore, there is a need for a technology to provide a simple, flexible, and efficient method to decompose the input space and enhance the capacity of the verification.
The present invention is a method and apparatus to verify a design which has an input space and a predicate. The input space is decomposed into a plurality of decompositions. The input space includes a plurality of node variables. The plurality of decompositions includes parametric variables. The decompositions are parameterized into vectors of parametric functions to satisfy the predicate.